Inference at * 2 1 1 
Iof proof for Lemma nth tl append:



1. T : Type
2. T List
3. T
4. v : T List
5. bs : T List
6. nth_tl(||v||;v @ bs) ~ bs
7. 0 < (||v||+1)
  nth_tl((||v||+1) - 1;v @ bs) ~ bs 

latex

 by ((NthHypSq (-2)) 
CollapseTHEN (ProveSqEq)) 

latex

C1: 

C1:   ((||v||+1) - 1) ~ ||v||
C.

Definitions

a < b, n+m, #$n, nth_tl(n;as), ||as||, as @ bs, type List, s ~ t, Type, n - m